\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]single{-}thread{-}generator\{i:l\}(${\it es}$;$P$;$R$)
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. ($R$($e$,${\it e'}$)) $\Rightarrow$ ($P$($e$) \& $P$(${\it e'}$)))
\\[0ex]$\Rightarrow$ \=(connex(\{$e$:E$\mid$ $P$($e$)\} ;$R$$^{\mbox{\scriptsize $\ast$}}$)\+
\\[0ex]c$\wedge$ ($R$\^{}+$\mid$$P$ $\Lleftarrow\!\Rrightarrow$\{E\} $x$,$y$:E. ($x$ $<$ $y$)$\mid$$P$)
\\[0ex]c$\wedge$ ($R$ $\Lleftarrow\!\Rrightarrow$\{E\} $R$\^{}+!)
\\[0ex]c$\wedge$ ($\forall$$x$, $y$, ${\it x'}$, ${\it y'}$:E. ($R$\^{}+($x$,$y$)) $\Rightarrow$ ($R$(${\it y'}$,$y$)) $\Rightarrow$ (($R$$^{\mbox{\scriptsize $\ast$}}$)($x$,${\it y'}$)))
\\[0ex]c$\wedge$ ($\forall$$x$, $y$, ${\it x'}$, ${\it y'}$:E. ($R$\^{}+($x$,$y$)) $\Rightarrow$ ($R$(${\it x'}$,$x$)) $\Rightarrow$ ($R$(${\it y'}$,$y$)) $\Rightarrow$ ($R$\^{}+(${\it x'}$,${\it y'}$))))
\-
\end{tabbing}